package sketch.specs.symbc;

import java.lang.reflect.Method;
import java.util.LinkedList;

import sketch.util.Checker;

import gov.nasa.jpf.symbc.TestExJPF;

public class SymbolicJPF extends TestExJPF{
	
	 protected static SymbolicJPF symbolicJPF = new SymbolicJPF();
	 
	 public static void execute(Class<?> driver, String methodName) {
		 symbolicJPF.runSymbolicJPF(driver, methodName);
	 }

	 public String[] JPFArgs(Class<?> driver, String methodName) {
		    Method testMethod = getTestMethod(driver, methodName);
		    Checker.checkNull(testMethod, "The method: " + methodName + " does not exist in class: " + driver);
		    checkmethodValidity(testMethod);
		    //create a list of jpf arguments
		    LinkedList<String> args = new LinkedList<String>();
		    //full fil the args
		    args.addAll(config);
		    args.add("+symbolic.method=" + methodName + "("
		        + allSymbolicArgs(getNumberofArguments(testMethod)) + ")");
		    args.add(driver.getName());

		    return args.toArray(new String[args.size()]);
	}
	 
	private void checkmethodValidity(Method m) {
		Checker.checkTrue(m.getParameterTypes().length != 0,
				"The parameter length could not be 0 for method: " + m.getName());
		for(Class<?> type : m.getParameterTypes()) {
			Checker.checkTrue(type.isPrimitive(), "Currently we only support primitive type, the given one is: " + type);
		}
	}
	 
	private Method getTestMethod(Class<?> c, String methodName) {
	   for (Method m : c.getMethods()) {
	     if (m.getName().equals(methodName)) {
	       return m;
	     }
	   }
      return null;
	}
	
	public void runSymbolicJPF(Class<?> driver, String symbolicMethodName) {
		runJPFnoException(JPFArgs(driver, symbolicMethodName));
	}
	
}
